$\forall$$M$:MsgA, $a$:Id, $s$:$M$.state, $v$:$M$.da(locl($a$)). $M$.pre($a$,$s$,$v$) $\in$ Prop